The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

eq(0, 0) → true [1]
eq(0, s(Y)) → false [1]
eq(s(X), 0) → false [1]
eq(s(X), s(Y)) → eq(X, Y) [1]
le(0, Y) → true [1]
le(s(X), 0) → false [1]
le(s(X), s(Y)) → le(X, Y) [1]
min(cons(0, nil)) → 0 [1]
min(cons(s(N), nil)) → s(N) [1]
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L))) [1]
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L)) [1]
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L)) [1]
replace(N, M, nil) → nil [1]
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L)) [1]
ifrepl(true, N, M, cons(K, L)) → cons(M, L) [1]
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L)) [1]
selsort(nil) → nil [1]
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L)) [1]
ifselsort(true, cons(N, L)) → cons(N, selsort(L)) [1]
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

eq(0, 0) → true [1]
eq(0, s(Y)) → false [1]
eq(s(X), 0) → false [1]
eq(s(X), s(Y)) → eq(X, Y) [1]
le(0, Y) → true [1]
le(s(X), 0) → false [1]
le(s(X), s(Y)) → le(X, Y) [1]
min(cons(0, nil)) → 0 [1]
min(cons(s(N), nil)) → s(N) [1]
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L))) [1]
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L)) [1]
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L)) [1]
replace(N, M, nil) → nil [1]
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L)) [1]
ifrepl(true, N, M, cons(K, L)) → cons(M, L) [1]
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L)) [1]
selsort(nil) → nil [1]
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L)) [1]
ifselsort(true, cons(N, L)) → cons(N, selsort(L)) [1]
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) [1]

The TRS has the following type information:

eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false le :: 0:s → 0:s → true:false min :: nil:cons → 0:s cons :: 0:s → nil:cons → nil:cons nil :: nil:cons ifmin :: true:false → nil:cons → 0:s replace :: 0:s → 0:s → nil:cons → nil:cons ifrepl :: true:false → 0:s → 0:s → nil:cons → nil:cons selsort :: nil:cons → nil:cons ifselsort :: true:false → nil:cons → nil:cons

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

selsort
ifselsort

(c) The following functions are completely defined:

le
eq
min
replace
ifmin
ifrepl

Due to the following rules being added:

min(v0) → 0 [0]
ifmin(v0, v1) → 0 [0]
ifrepl(v0, v1, v2, v3) → nil [0]

And the following fresh constants: none

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) → true [1] eq(0, s(Y)) → false [1] eq(s(X), 0) → false [1] eq(s(X), s(Y)) → eq(X, Y) [1] le(0, Y) → true [1] le(s(X), 0) → false [1] le(s(X), s(Y)) → le(X, Y) [1] min(cons(0, nil)) → 0 [1] min(cons(s(N), nil)) → s(N) [1] min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L))) [1] ifmin(true, cons(N, cons(M, L))) → min(cons(N, L)) [1] ifmin(false, cons(N, cons(M, L))) → min(cons(M, L)) [1] replace(N, M, nil) → nil [1] replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L)) [1] ifrepl(true, N, M, cons(K, L)) → cons(M, L) [1] ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L)) [1] selsort(nil) → nil [1] selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L)) [1] ifselsort(true, cons(N, L)) → cons(N, selsort(L)) [1] ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) [1] min(v0) → 0 [0] ifmin(v0, v1) → 0 [0] ifrepl(v0, v1, v2, v3) → nil [0] The TRS has the following type information: eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false le :: 0:s → 0:s → true:false min :: nil:cons → 0:s cons :: 0:s → nil:cons → nil:cons nil :: nil:cons ifmin :: true:false → nil:cons → 0:s replace :: 0:s → 0:s → nil:cons → nil:cons ifrepl :: true:false → 0:s → 0:s → nil:cons → nil:cons selsort :: nil:cons → nil:cons ifselsort :: true:false → nil:cons → nil:cons Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: eq(0, 0) → true [1] eq(0, s(Y)) → false [1] eq(s(X), 0) → false [1] eq(s(X), s(Y)) → eq(X, Y) [1] le(0, Y) → true [1] le(s(X), 0) → false [1] le(s(X), s(Y)) → le(X, Y) [1] min(cons(0, nil)) → 0 [1] min(cons(s(N), nil)) → s(N) [1] min(cons(0, cons(M, L))) → ifmin(true, cons(0, cons(M, L))) [2] min(cons(s(X'), cons(0, L))) → ifmin(false, cons(s(X'), cons(0, L))) [2] min(cons(s(X''), cons(s(Y'), L))) → ifmin(le(X'', Y'), cons(s(X''), cons(s(Y'), L))) [2] ifmin(true, cons(N, cons(M, L))) → min(cons(N, L)) [1] ifmin(false, cons(N, cons(M, L))) → min(cons(M, L)) [1] replace(N, M, nil) → nil [1] replace(0, M, cons(0, L)) → ifrepl(true, 0, M, cons(0, L)) [2] replace(0, M, cons(s(Y''), L)) → ifrepl(false, 0, M, cons(s(Y''), L)) [2] replace(s(X1), M, cons(0, L)) → ifrepl(false, s(X1), M, cons(0, L)) [2] replace(s(X2), M, cons(s(Y1), L)) → ifrepl(eq(X2, Y1), s(X2), M, cons(s(Y1), L)) [2] ifrepl(true, N, M, cons(K, L)) → cons(M, L) [1] ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L)) [1] selsort(nil) → nil [1] selsort(cons(0, nil)) → ifselsort(eq(0, 0), cons(0, nil)) [2] selsort(cons(s(N'), nil)) → ifselsort(eq(s(N'), s(N')), cons(s(N'), nil)) [2] selsort(cons(N, cons(M', L'))) → ifselsort(eq(N, ifmin(le(N, M'), cons(N, cons(M', L')))), cons(N, cons(M', L'))) [2] selsort(cons(N, L)) → ifselsort(eq(N, 0), cons(N, L)) [1] ifselsort(true, cons(N, L)) → cons(N, selsort(L)) [1] ifselsort(false, cons(0, nil)) → cons(min(cons(0, nil)), selsort(replace(0, 0, nil))) [2] ifselsort(false, cons(s(N''), nil)) → cons(min(cons(s(N''), nil)), selsort(replace(s(N''), s(N''), nil))) [2] ifselsort(false, cons(N, cons(M'', L''))) → cons(min(cons(N, cons(M'', L''))), selsort(replace(ifmin(le(N, M''), cons(N, cons(M'', L''))), N, cons(M'', L'')))) [2] ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(0, N, L))) [1] min(v0) → 0 [0] ifmin(v0, v1) → 0 [0] ifrepl(v0, v1, v2, v3) → nil [0] The TRS has the following type information: eq :: 0:s → 0:s → true:false 0 :: 0:s true :: true:false s :: 0:s → 0:s false :: true:false le :: 0:s → 0:s → true:false min :: nil:cons → 0:s cons :: 0:s → nil:cons → nil:cons nil :: nil:cons ifmin :: true:false → nil:cons → 0:s replace :: 0:s → 0:s → nil:cons → nil:cons ifrepl :: true:false → 0:s → 0:s → nil:cons → nil:cons selsort :: nil:cons → nil:cons ifselsort :: true:false → nil:cons → nil:cons Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
true => 1
false => 0
nil => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: Y >= 0, z' = 1 + Y, z = 0
eq(z, z') -{ 1 }→ 0 :|: z = 1 + X, X >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(N, M, L) :|: K >= 0, z' = N, L >= 0, z = 0, M >= 0, z'' = M, z1 = 1 + K + L, N >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + M + L :|: z = 1, K >= 0, z' = N, L >= 0, M >= 0, z'' = M, z1 = 1 + K + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(le(N, M''), 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + N'') + 0) + selsort(replace(1 + N'', 1 + N'', 0)) :|: z' = 1 + (1 + N'') + 0, N'' >= 0, z = 0
le(z, z') -{ 1 }→ le(X, Y) :|: z = 1 + X, Y >= 0, z' = 1 + Y, X >= 0
le(z, z') -{ 1 }→ 1 :|: z' = Y, Y >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z = 1 + X, X >= 0, z' = 0
min(z) -{ 2 }→ ifmin(le(X'', Y'), 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
min(z) -{ 1 }→ 1 + N :|: z = 1 + (1 + N) + 0, N >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(X2, Y1), 1 + X2, M, 1 + (1 + Y1) + L) :|: z' = M, Y1 >= 0, z'' = 1 + (1 + Y1) + L, z = 1 + X2, L >= 0, X2 >= 0, M >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, M, 1 + 0 + L) :|: z'' = 1 + 0 + L, z' = M, L >= 0, z = 0, M >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, M, 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, z' = M, Y'' >= 0, L >= 0, z = 0, M >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + X1, M, 1 + 0 + L) :|: z'' = 1 + 0 + L, X1 >= 0, z' = M, z = 1 + X1, L >= 0, M >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' = M, z = N, M >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(N, ifmin(le(N, M'), 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + N', 1 + N'), 1 + (1 + N') + 0) :|: z = 1 + (1 + N') + 0, N' >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(le(N, M''), 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 2 }→ ifmin(le(X'', Y'), 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 2 }→ ifselsort(eq(N, ifmin(le(N, M'), 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ le } { eq } { min, ifmin } { replace, ifrepl } { ifselsort, selsort }

(14) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(le(N, M''), 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 2 }→ ifmin(le(X'', Y'), 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 2 }→ ifselsort(eq(N, ifmin(le(N, M'), 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {le}, {eq}, {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: le
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(16) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(le(N, M''), 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 2 }→ ifmin(le(X'', Y'), 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 2 }→ ifselsort(eq(N, ifmin(le(N, M'), 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {le}, {eq}, {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: ?, size: O(1) [1]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: le
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(18) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(le(N, M''), 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 }→ le(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 2 }→ ifmin(le(X'', Y'), 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 2 }→ ifselsort(eq(N, ifmin(le(N, M'), 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {eq}, {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {eq}, {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: eq
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {eq}, {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: ?, size: O(1) [1]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: eq
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z'

(24) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 }→ eq(z - 1, z' - 1) :|: z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(eq(z - 1, Y1), 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ ifselsort(eq(N, 0), 1 + N + L) :|: z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 2 }→ ifselsort(eq(0, 0), 1 + 0 + 0) :|: z = 1 + 0 + 0
selsort(z) -{ 2 }→ ifselsort(eq(1 + (z - 2), 1 + (z - 2)), 1 + (1 + (z - 2)) + 0) :|: z - 2 >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: min
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

Computed SIZE bound using KoAT for: ifmin
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'

(28) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {min,ifmin}, {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: ?, size: O(n1) [z] ifmin: runtime: ?, size: O(n1) [z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: min
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 2 + 18·z + 2·z²

Computed RUNTIME bound using KoAT for: ifmin
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 46 + 88·z' + 16·z'²

(30) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 1 }→ min(1 + M + L) :|: z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 1 }→ min(1 + N + L) :|: z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 1 }→ 1 + min(1 + N + L) + selsort(replace(0, N, L)) :|: L >= 0, z = 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 3 + M'' }→ 1 + min(1 + N + (1 + M'' + L'')) + selsort(replace(ifmin(s1, 1 + N + (1 + M'' + L'')), N, 1 + M'' + L'')) :|: s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + 0 + 0) + selsort(replace(0, 0, 0)) :|: z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 2 }→ 1 + min(1 + (1 + (z' - 2)) + 0) + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: z' - 2 >= 0, z = 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 3 + Y' }→ ifmin(s', 1 + (1 + X'') + (1 + (1 + Y') + L)) :|: s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 2 }→ ifmin(1, 1 + 0 + (1 + M + L)) :|: z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 2 }→ ifmin(0, 1 + (1 + X') + (1 + 0 + L)) :|: X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 3 + M' }→ ifselsort(eq(N, ifmin(s'', 1 + N + (1 + M' + L'))), 1 + N + (1 + M' + L')) :|: s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z']

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 24 }→ 1 + s14 + selsort(replace(0, 0, 0)) :|: s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 4 + 18·z' + 2·z'² }→ 1 + s15 + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 335 + 178·L'' + 36·L''·M'' + 36·L''·N + 18·L''² + 179·M'' + 36·M''·N + 18·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(replace(s17, N, 1 + M'' + L'')) :|: s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ 1 + s18 + selsort(replace(0, N, L)) :|: s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: replace
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z' + z''

Computed SIZE bound using KoAT for: ifrepl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z'' + z1

(34) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 24 }→ 1 + s14 + selsort(replace(0, 0, 0)) :|: s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 4 + 18·z' + 2·z'² }→ 1 + s15 + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 335 + 178·L'' + 36·L''·M'' + 36·L''·N + 18·L''² + 179·M'' + 36·M''·N + 18·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(replace(s17, N, 1 + M'' + L'')) :|: s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ 1 + s18 + selsort(replace(0, N, L)) :|: s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {replace,ifrepl}, {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z'] replace: runtime: ?, size: O(n1) [z' + z''] ifrepl: runtime: ?, size: O(n1) [z'' + z1]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: replace
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 2 + 20·z'' + 2·z''²

Computed RUNTIME bound using KoAT for: ifrepl
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 4 + 20·z1 + 2·z1²

(36) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + K + replace(z', z'', L) :|: K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 24 }→ 1 + s14 + selsort(replace(0, 0, 0)) :|: s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 4 + 18·z' + 2·z'² }→ 1 + s15 + selsort(replace(1 + (z' - 2), 1 + (z' - 2), 0)) :|: s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 335 + 178·L'' + 36·L''·M'' + 36·L''·N + 18·L''² + 179·M'' + 36·M''·N + 18·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(replace(s17, N, 1 + M'' + L'')) :|: s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ 1 + s18 + selsort(replace(0, N, L)) :|: s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 3 + Y1 }→ ifrepl(s3, 1 + (z - 1), z', 1 + (1 + Y1) + L) :|: s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(1, 0, z', 1 + 0 + (z'' - 1)) :|: z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 0, z', 1 + (1 + Y'') + L) :|: z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 2 }→ ifrepl(0, 1 + (z - 1), z', 1 + 0 + (z'' - 1)) :|: z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z'] replace: runtime: O(n2) [2 + 20·z'' + 2·z''2], size: O(n1) [z' + z''] ifrepl: runtime: O(n2) [4 + 20·z1 + 2·z12], size: O(n1) [z'' + z1]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 3 + 20·L + 2·L² }→ 1 + K + s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * L, K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 26 }→ 1 + s14 + selsort(s24) :|: s24 >= 0, s24 <= 1 * 0 + 1 * 0, s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 6 + 18·z' + 2·z'² }→ 1 + s15 + selsort(s25) :|: s25 >= 0, s25 <= 1 * (1 + (z' - 2)) + 1 * 0, s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 359 + 202·L'' + 40·L''·M'' + 36·L''·N + 20·L''² + 203·M'' + 36·M''·N + 20·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(s26) :|: s26 >= 0, s26 <= 1 * N + 1 * (1 + M'' + L''), s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 25 + 42·L + 4·L·N + 4·L² + 22·N + 2·N² }→ 1 + s18 + selsort(s27) :|: s27 >= 0, s27 <= 1 * N + 1 * L, s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s19 :|: s19 >= 0, s19 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 54 + 28·L + 4·L·Y'' + 2·L² + 28·Y'' + 2·Y''² }→ s20 :|: s20 >= 0, s20 <= 1 * z' + 1 * (1 + (1 + Y'') + L), z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s21 :|: s21 >= 0, s21 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 55 + 28·L + 4·L·Y1 + 2·L² + 29·Y1 + 2·Y1² }→ s22 :|: s22 >= 0, s22 <= 1 * z' + 1 * (1 + (1 + Y1) + L), s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z'] replace: runtime: O(n2) [2 + 20·z'' + 2·z''2], size: O(n1) [z' + z''] ifrepl: runtime: O(n2) [4 + 20·z1 + 2·z12], size: O(n1) [z'' + z1]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: ifselsort
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 20·z' + 8·z'²

Computed SIZE bound using KoAT for: selsort
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 128 + 248·z + 112·z²

(40) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 3 + 20·L + 2·L² }→ 1 + K + s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * L, K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 26 }→ 1 + s14 + selsort(s24) :|: s24 >= 0, s24 <= 1 * 0 + 1 * 0, s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 6 + 18·z' + 2·z'² }→ 1 + s15 + selsort(s25) :|: s25 >= 0, s25 <= 1 * (1 + (z' - 2)) + 1 * 0, s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 359 + 202·L'' + 40·L''·M'' + 36·L''·N + 20·L''² + 203·M'' + 36·M''·N + 20·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(s26) :|: s26 >= 0, s26 <= 1 * N + 1 * (1 + M'' + L''), s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 25 + 42·L + 4·L·N + 4·L² + 22·N + 2·N² }→ 1 + s18 + selsort(s27) :|: s27 >= 0, s27 <= 1 * N + 1 * L, s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s19 :|: s19 >= 0, s19 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 54 + 28·L + 4·L·Y'' + 2·L² + 28·Y'' + 2·Y''² }→ s20 :|: s20 >= 0, s20 <= 1 * z' + 1 * (1 + (1 + Y'') + L), z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s21 :|: s21 >= 0, s21 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 55 + 28·L + 4·L·Y1 + 2·L² + 29·Y1 + 2·Y1² }→ s22 :|: s22 >= 0, s22 <= 1 * z' + 1 * (1 + (1 + Y1) + L), s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed: {ifselsort,selsort}
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z'] replace: runtime: O(n2) [2 + 20·z'' + 2·z''2], size: O(n1) [z' + z''] ifrepl: runtime: O(n2) [4 + 20·z1 + 2·z12], size: O(n1) [z'' + z1] ifselsort: runtime: ?, size: O(n2) [20·z' + 8·z'2] selsort: runtime: ?, size: O(n2) [128 + 248·z + 112·z2]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: ifselsort
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 1 + 4336·z' + 3556·z'² + 652·z'³

Computed RUNTIME bound using KoAT for: selsort
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 45504 + 110757·z + 92960·z² + 23472·z³

(42) Obligation:

Complexity RNTS consisting of the following rules:

eq(z, z') -{ 1 + z' }→ s2 :|: s2 >= 0, s2 <= 1, z' - 1 >= 0, z - 1 >= 0
eq(z, z') -{ 1 }→ 1 :|: z = 0, z' = 0
eq(z, z') -{ 1 }→ 0 :|: z' - 1 >= 0, z = 0
eq(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
ifmin(z, z') -{ 23 + 22·L + 4·L·N + 2·L² + 22·N + 2·N² }→ s10 :|: s10 >= 0, s10 <= 1 * (1 + N + L), z = 1, z' = 1 + N + (1 + M + L), L >= 0, M >= 0, N >= 0
ifmin(z, z') -{ 23 + 22·L + 4·L·M + 2·L² + 22·M + 2·M² }→ s11 :|: s11 >= 0, s11 <= 1 * (1 + M + L), z' = 1 + N + (1 + M + L), L >= 0, z = 0, M >= 0, N >= 0
ifmin(z, z') -{ 0 }→ 0 :|: z >= 0, z' >= 0
ifrepl(z, z', z'', z1) -{ 0 }→ 0 :|: z >= 0, z' >= 0, z'' >= 0, z1 >= 0
ifrepl(z, z', z'', z1) -{ 3 + 20·L + 2·L² }→ 1 + K + s23 :|: s23 >= 0, s23 <= 1 * z'' + 1 * L, K >= 0, L >= 0, z = 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifrepl(z, z', z'', z1) -{ 1 }→ 1 + z'' + L :|: z = 1, K >= 0, L >= 0, z'' >= 0, z1 = 1 + K + L, z' >= 0
ifselsort(z, z') -{ 1 }→ 1 + N + selsort(L) :|: z = 1, L >= 0, z' = 1 + N + L, N >= 0
ifselsort(z, z') -{ 26 }→ 1 + s14 + selsort(s24) :|: s24 >= 0, s24 <= 1 * 0 + 1 * 0, s14 >= 0, s14 <= 1 * (1 + 0 + 0), z' = 1 + 0 + 0, z = 0
ifselsort(z, z') -{ 6 + 18·z' + 2·z'² }→ 1 + s15 + selsort(s25) :|: s25 >= 0, s25 <= 1 * (1 + (z' - 2)) + 1 * 0, s15 >= 0, s15 <= 1 * (1 + (1 + (z' - 2)) + 0), z' - 2 >= 0, z = 0
ifselsort(z, z') -{ 359 + 202·L'' + 40·L''·M'' + 36·L''·N + 20·L''² + 203·M'' + 36·M''·N + 20·M''² + 178·N + 18·N² }→ 1 + s16 + selsort(s26) :|: s26 >= 0, s26 <= 1 * N + 1 * (1 + M'' + L''), s16 >= 0, s16 <= 1 * (1 + N + (1 + M'' + L'')), s17 >= 0, s17 <= 1 * (1 + N + (1 + M'' + L'')), s1 >= 0, s1 <= 1, L'' >= 0, M'' >= 0, z' = 1 + N + (1 + M'' + L''), z = 0, N >= 0
ifselsort(z, z') -{ 25 + 42·L + 4·L·N + 4·L² + 22·N + 2·N² }→ 1 + s18 + selsort(s27) :|: s27 >= 0, s27 <= 1 * N + 1 * L, s18 >= 0, s18 <= 1 * (1 + N + L), L >= 0, z = 0, z' = 1 + N + L, N >= 0
le(z, z') -{ 1 + z' }→ s :|: s >= 0, s <= 1, z' - 1 >= 0, z - 1 >= 0
le(z, z') -{ 1 }→ 1 :|: z' >= 0, z = 0
le(z, z') -{ 1 }→ 0 :|: z - 1 >= 0, z' = 0
min(z) -{ 288 + 152·L + 32·L·M + 16·L² + 152·M + 16·M² }→ s7 :|: s7 >= 0, s7 <= 1 * (1 + 0 + (1 + M + L)), z = 1 + 0 + (1 + M + L), L >= 0, M >= 0
min(z) -{ 456 + 184·L + 32·L·X' + 16·L² + 184·X' + 16·X'² }→ s8 :|: s8 >= 0, s8 <= 1 * (1 + (1 + X') + (1 + 0 + L)), X' >= 0, L >= 0, z = 1 + (1 + X') + (1 + 0 + L)
min(z) -{ 657 + 216·L + 32·L·X'' + 32·L·Y' + 16·L² + 216·X'' + 32·X''·Y' + 16·X''² + 217·Y' + 16·Y'² }→ s9 :|: s9 >= 0, s9 <= 1 * (1 + (1 + X'') + (1 + (1 + Y') + L)), s' >= 0, s' <= 1, z = 1 + (1 + X'') + (1 + (1 + Y') + L), Y' >= 0, X'' >= 0, L >= 0
min(z) -{ 1 }→ 0 :|: z = 1 + 0 + 0
min(z) -{ 0 }→ 0 :|: z >= 0
min(z) -{ 1 }→ 1 + (z - 2) :|: z - 2 >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s19 :|: s19 >= 0, s19 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z'' - 1 >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 54 + 28·L + 4·L·Y'' + 2·L² + 28·Y'' + 2·Y''² }→ s20 :|: s20 >= 0, s20 <= 1 * z' + 1 * (1 + (1 + Y'') + L), z'' = 1 + (1 + Y'') + L, Y'' >= 0, L >= 0, z = 0, z' >= 0
replace(z, z', z'') -{ 6 + 20·z'' + 2·z''² }→ s21 :|: s21 >= 0, s21 <= 1 * z' + 1 * (1 + 0 + (z'' - 1)), z - 1 >= 0, z'' - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 55 + 28·L + 4·L·Y1 + 2·L² + 29·Y1 + 2·Y1² }→ s22 :|: s22 >= 0, s22 <= 1 * z' + 1 * (1 + (1 + Y1) + L), s3 >= 0, s3 <= 1, Y1 >= 0, z'' = 1 + (1 + Y1) + L, L >= 0, z - 1 >= 0, z' >= 0
replace(z, z', z'') -{ 1 }→ 0 :|: z'' = 0, z' >= 0, z >= 0
selsort(z) -{ 290 + 152·L' + 32·L'·M' + 32·L'·N + 16·L'² + 153·M' + 32·M'·N + 16·M'² + 152·N + 16·N² + s12 }→ ifselsort(s13, 1 + N + (1 + M' + L')) :|: s12 >= 0, s12 <= 1 * (1 + N + (1 + M' + L')), s13 >= 0, s13 <= 1, s'' >= 0, s'' <= 1, L' >= 0, z = 1 + N + (1 + M' + L'), M' >= 0, N >= 0
selsort(z) -{ 3 }→ ifselsort(s4, 1 + 0 + 0) :|: s4 >= 0, s4 <= 1, z = 1 + 0 + 0
selsort(z) -{ 2 + z }→ ifselsort(s5, 1 + (1 + (z - 2)) + 0) :|: s5 >= 0, s5 <= 1, z - 2 >= 0
selsort(z) -{ 2 }→ ifselsort(s6, 1 + N + L) :|: s6 >= 0, s6 <= 1, z = 1 + N + L, L >= 0, N >= 0
selsort(z) -{ 1 }→ 0 :|: z = 0

Function symbols to be analyzed:
Previous analysis results are:

le: runtime: O(n1) [1 + z'], size: O(1) [1] eq: runtime: O(n1) [1 + z'], size: O(1) [1] min: runtime: O(n2) [2 + 18·z + 2·z2], size: O(n1) [z] ifmin: runtime: O(n2) [46 + 88·z' + 16·z'2], size: O(n1) [z'] replace: runtime: O(n2) [2 + 20·z'' + 2·z''2], size: O(n1) [z' + z''] ifrepl: runtime: O(n2) [4 + 20·z1 + 2·z12], size: O(n1) [z'' + z1] ifselsort: runtime: O(n3) [1 + 4336·z' + 3556·z'2 + 652·z'3], size: O(n2) [20·z' + 8·z'2] selsort: runtime: O(n3) [45504 + 110757·z + 92960·z2 + 23472·z3], size: O(n2) [128 + 248·z + 112·z2]

(43) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(44) BOUNDS(1, n^3)